$\forall$$A$, ${\it A'}$:Type\{i\}, $B$:($A$$\rightarrow$Type\{j\}), $f$:($x$:$A$$\rightarrow$$B$($x$)). (${\it A'}$ $\subseteq$r $A$) $\Rightarrow$ ($f$ $\in$ $x$:${\it A'}$$\rightarrow$$B$($x$))